r:Rng, n:, u:|r|. (n r u)  |r| 

latex

Up	rings 1
Definitions of Statement	Rng, r+gp, n r e
Definitions	t.1, |g|, IMonoid, r+gp, n r e, t  T, x:A. B(x), , P & Q, Mon, Group{i}, AbGrp, Rng, S  T
Lemmas	rng wf, nat wf, rng car wf, add grp of rng wf, nat inc, abgrp wf, grp id wf, grp op wf, grp car wf, monoid p wf, add grp of rng wf b, mon nat op wf2